(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun T2_460 () (_ BitVec 16))
(declare-fun T4_464 () (_ BitVec 32))
(declare-fun T1_464 () (_ BitVec 8))
(declare-fun T1_465 () (_ BitVec 8))
(declare-fun T1_466 () (_ BitVec 8))
(declare-fun T1_467 () (_ BitVec 8))
(declare-fun T1_460 () (_ BitVec 8))
(declare-fun T1_461 () (_ BitVec 8))
(assert (let ((?v_0 ((_ zero_extend 16) T2_460))) (let ((?v_1 (bvadd ?v_0 (_ bv78 32)))) (and true (= T2_460 (bvor (bvshl ((_ zero_extend 8) T1_461) (_ bv8 16)) ((_ zero_extend 8) T1_460))) (= T4_464 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_467) (_ bv8 32)) ((_ zero_extend 24) T1_466)) (_ bv8 32)) ((_ zero_extend 24) T1_465)) (_ bv8 32)) ((_ zero_extend 24) T1_464))) (bvult (bvadd ?v_1 T4_464) T4_464) (bvult (bvsub (_ bv40 32) ?v_0) (_ bv63 32)) (bvult ?v_0 (_ bv256 32)) (bvult ?v_0 (_ bv2147483648 32)) (bvule ?v_0 (_ bv2147483647 32)) (not (= ?v_0 (_ bv0 32))) (bvule ?v_0 (_ bv4294967264 32)) (bvule ?v_0 ?v_1)))))
(check-sat)
(exit)
